more on commutator subgroups #2205
Conversation
Signed-off-by: Ali Caglayan <alizter@gmail.com> <!-- ps-id: 227461ec-4379-4d51-8913-796c057fdd83 -->
| Definition subgroup_commutator_normal_prod_l {G : Group} | ||
| (H K L : NormalSubgroup G) | ||
| : forall x, [subgroup_product H K, L] x <-> subgroup_product [H, L] [K, L] x. |
There was a problem hiding this comment.
Does this really require all three to be normal? Where is normality used in the proof?
There was a problem hiding this comment.
When we precompose with a commutator the subgroup needs to be normal for the whole predicate to be a subgroup. We need the target to be a subgroup for the subgroup_commutator_rec lemma to be applied.
I got this statement as exercise 5.1.5 in J.S. Robinson's "A Course In the Theory of Groups". There it is stated as all subgroups being normal, but it is not clear if that is necessary.
I can easily come up with counter examples where none of the subgroups are normal, but I haven't been able to come up with one where only one is non-normal.
There was a problem hiding this comment.
I did a beefier search (with GAP) where 2 subgroups where normal and the other was not and I was not able to find any counter examples. I'll need to find some spare time to think about this more deeply.
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
No description provided.